(0) Obligation:
Clauses:
perm1(L, M) :- ','(eq_len1(L, M), same_sets(L, M)).
eq_len1([], []).
eq_len1(.(X1, Xs), .(X2, Ys)) :- eq_len1(Xs, Ys).
member(X, .(X, X3)).
member(X, .(X4, T)) :- member(X, T).
same_sets([], X5).
same_sets(.(X, Xs), L) :- ','(member(X, L), same_sets(Xs, L)).
Query: perm1(g,g)
(1) PrologToPiTRSProof (SOUND transformation)
We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
perm1_in: (b,b)
eq_len1_in: (b,b)
same_sets_in: (b,b)
member_in: (b,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X1, Xs), .(X2, Ys)) → U3_gg(X1, Xs, X2, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X1, Xs, X2, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X1, Xs), .(X2, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X5) → same_sets_out_gg([], X5)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, T)) → U4_gg(X, X4, T, member_in_gg(X, T))
U4_gg(X, X4, T, member_out_gg(X, T)) → member_out_gg(X, .(X4, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)
The argument filtering Pi contains the following mapping:
perm1_in_gg(
x1,
x2) =
perm1_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
eq_len1_in_gg(
x1,
x2) =
eq_len1_in_gg(
x1,
x2)
[] =
[]
eq_len1_out_gg(
x1,
x2) =
eq_len1_out_gg
.(
x1,
x2) =
.(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5) =
U3_gg(
x5)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x3)
same_sets_in_gg(
x1,
x2) =
same_sets_in_gg(
x1,
x2)
same_sets_out_gg(
x1,
x2) =
same_sets_out_gg
U5_gg(
x1,
x2,
x3,
x4) =
U5_gg(
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
U6_gg(
x1,
x2,
x3,
x4) =
U6_gg(
x4)
perm1_out_gg(
x1,
x2) =
perm1_out_gg
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(2) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X1, Xs), .(X2, Ys)) → U3_gg(X1, Xs, X2, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X1, Xs, X2, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X1, Xs), .(X2, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X5) → same_sets_out_gg([], X5)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, T)) → U4_gg(X, X4, T, member_in_gg(X, T))
U4_gg(X, X4, T, member_out_gg(X, T)) → member_out_gg(X, .(X4, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)
The argument filtering Pi contains the following mapping:
perm1_in_gg(
x1,
x2) =
perm1_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
eq_len1_in_gg(
x1,
x2) =
eq_len1_in_gg(
x1,
x2)
[] =
[]
eq_len1_out_gg(
x1,
x2) =
eq_len1_out_gg
.(
x1,
x2) =
.(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5) =
U3_gg(
x5)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x3)
same_sets_in_gg(
x1,
x2) =
same_sets_in_gg(
x1,
x2)
same_sets_out_gg(
x1,
x2) =
same_sets_out_gg
U5_gg(
x1,
x2,
x3,
x4) =
U5_gg(
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
U6_gg(
x1,
x2,
x3,
x4) =
U6_gg(
x4)
perm1_out_gg(
x1,
x2) =
perm1_out_gg
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
PERM1_IN_GG(L, M) → U1_GG(L, M, eq_len1_in_gg(L, M))
PERM1_IN_GG(L, M) → EQ_LEN1_IN_GG(L, M)
EQ_LEN1_IN_GG(.(X1, Xs), .(X2, Ys)) → U3_GG(X1, Xs, X2, Ys, eq_len1_in_gg(Xs, Ys))
EQ_LEN1_IN_GG(.(X1, Xs), .(X2, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)
U1_GG(L, M, eq_len1_out_gg(L, M)) → U2_GG(L, M, same_sets_in_gg(L, M))
U1_GG(L, M, eq_len1_out_gg(L, M)) → SAME_SETS_IN_GG(L, M)
SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(X, Xs, L, member_in_gg(X, L))
SAME_SETS_IN_GG(.(X, Xs), L) → MEMBER_IN_GG(X, L)
MEMBER_IN_GG(X, .(X4, T)) → U4_GG(X, X4, T, member_in_gg(X, T))
MEMBER_IN_GG(X, .(X4, T)) → MEMBER_IN_GG(X, T)
U5_GG(X, Xs, L, member_out_gg(X, L)) → U6_GG(X, Xs, L, same_sets_in_gg(Xs, L))
U5_GG(X, Xs, L, member_out_gg(X, L)) → SAME_SETS_IN_GG(Xs, L)
The TRS R consists of the following rules:
perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X1, Xs), .(X2, Ys)) → U3_gg(X1, Xs, X2, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X1, Xs, X2, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X1, Xs), .(X2, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X5) → same_sets_out_gg([], X5)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, T)) → U4_gg(X, X4, T, member_in_gg(X, T))
U4_gg(X, X4, T, member_out_gg(X, T)) → member_out_gg(X, .(X4, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)
The argument filtering Pi contains the following mapping:
perm1_in_gg(
x1,
x2) =
perm1_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
eq_len1_in_gg(
x1,
x2) =
eq_len1_in_gg(
x1,
x2)
[] =
[]
eq_len1_out_gg(
x1,
x2) =
eq_len1_out_gg
.(
x1,
x2) =
.(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5) =
U3_gg(
x5)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x3)
same_sets_in_gg(
x1,
x2) =
same_sets_in_gg(
x1,
x2)
same_sets_out_gg(
x1,
x2) =
same_sets_out_gg
U5_gg(
x1,
x2,
x3,
x4) =
U5_gg(
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
U6_gg(
x1,
x2,
x3,
x4) =
U6_gg(
x4)
perm1_out_gg(
x1,
x2) =
perm1_out_gg
PERM1_IN_GG(
x1,
x2) =
PERM1_IN_GG(
x1,
x2)
U1_GG(
x1,
x2,
x3) =
U1_GG(
x1,
x2,
x3)
EQ_LEN1_IN_GG(
x1,
x2) =
EQ_LEN1_IN_GG(
x1,
x2)
U3_GG(
x1,
x2,
x3,
x4,
x5) =
U3_GG(
x5)
U2_GG(
x1,
x2,
x3) =
U2_GG(
x3)
SAME_SETS_IN_GG(
x1,
x2) =
SAME_SETS_IN_GG(
x1,
x2)
U5_GG(
x1,
x2,
x3,
x4) =
U5_GG(
x2,
x3,
x4)
MEMBER_IN_GG(
x1,
x2) =
MEMBER_IN_GG(
x1,
x2)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x4)
U6_GG(
x1,
x2,
x3,
x4) =
U6_GG(
x4)
We have to consider all (P,R,Pi)-chains
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PERM1_IN_GG(L, M) → U1_GG(L, M, eq_len1_in_gg(L, M))
PERM1_IN_GG(L, M) → EQ_LEN1_IN_GG(L, M)
EQ_LEN1_IN_GG(.(X1, Xs), .(X2, Ys)) → U3_GG(X1, Xs, X2, Ys, eq_len1_in_gg(Xs, Ys))
EQ_LEN1_IN_GG(.(X1, Xs), .(X2, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)
U1_GG(L, M, eq_len1_out_gg(L, M)) → U2_GG(L, M, same_sets_in_gg(L, M))
U1_GG(L, M, eq_len1_out_gg(L, M)) → SAME_SETS_IN_GG(L, M)
SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(X, Xs, L, member_in_gg(X, L))
SAME_SETS_IN_GG(.(X, Xs), L) → MEMBER_IN_GG(X, L)
MEMBER_IN_GG(X, .(X4, T)) → U4_GG(X, X4, T, member_in_gg(X, T))
MEMBER_IN_GG(X, .(X4, T)) → MEMBER_IN_GG(X, T)
U5_GG(X, Xs, L, member_out_gg(X, L)) → U6_GG(X, Xs, L, same_sets_in_gg(Xs, L))
U5_GG(X, Xs, L, member_out_gg(X, L)) → SAME_SETS_IN_GG(Xs, L)
The TRS R consists of the following rules:
perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X1, Xs), .(X2, Ys)) → U3_gg(X1, Xs, X2, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X1, Xs, X2, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X1, Xs), .(X2, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X5) → same_sets_out_gg([], X5)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, T)) → U4_gg(X, X4, T, member_in_gg(X, T))
U4_gg(X, X4, T, member_out_gg(X, T)) → member_out_gg(X, .(X4, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)
The argument filtering Pi contains the following mapping:
perm1_in_gg(
x1,
x2) =
perm1_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
eq_len1_in_gg(
x1,
x2) =
eq_len1_in_gg(
x1,
x2)
[] =
[]
eq_len1_out_gg(
x1,
x2) =
eq_len1_out_gg
.(
x1,
x2) =
.(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5) =
U3_gg(
x5)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x3)
same_sets_in_gg(
x1,
x2) =
same_sets_in_gg(
x1,
x2)
same_sets_out_gg(
x1,
x2) =
same_sets_out_gg
U5_gg(
x1,
x2,
x3,
x4) =
U5_gg(
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
U6_gg(
x1,
x2,
x3,
x4) =
U6_gg(
x4)
perm1_out_gg(
x1,
x2) =
perm1_out_gg
PERM1_IN_GG(
x1,
x2) =
PERM1_IN_GG(
x1,
x2)
U1_GG(
x1,
x2,
x3) =
U1_GG(
x1,
x2,
x3)
EQ_LEN1_IN_GG(
x1,
x2) =
EQ_LEN1_IN_GG(
x1,
x2)
U3_GG(
x1,
x2,
x3,
x4,
x5) =
U3_GG(
x5)
U2_GG(
x1,
x2,
x3) =
U2_GG(
x3)
SAME_SETS_IN_GG(
x1,
x2) =
SAME_SETS_IN_GG(
x1,
x2)
U5_GG(
x1,
x2,
x3,
x4) =
U5_GG(
x2,
x3,
x4)
MEMBER_IN_GG(
x1,
x2) =
MEMBER_IN_GG(
x1,
x2)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x4)
U6_GG(
x1,
x2,
x3,
x4) =
U6_GG(
x4)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 8 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MEMBER_IN_GG(X, .(X4, T)) → MEMBER_IN_GG(X, T)
The TRS R consists of the following rules:
perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X1, Xs), .(X2, Ys)) → U3_gg(X1, Xs, X2, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X1, Xs, X2, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X1, Xs), .(X2, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X5) → same_sets_out_gg([], X5)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, T)) → U4_gg(X, X4, T, member_in_gg(X, T))
U4_gg(X, X4, T, member_out_gg(X, T)) → member_out_gg(X, .(X4, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)
The argument filtering Pi contains the following mapping:
perm1_in_gg(
x1,
x2) =
perm1_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
eq_len1_in_gg(
x1,
x2) =
eq_len1_in_gg(
x1,
x2)
[] =
[]
eq_len1_out_gg(
x1,
x2) =
eq_len1_out_gg
.(
x1,
x2) =
.(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5) =
U3_gg(
x5)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x3)
same_sets_in_gg(
x1,
x2) =
same_sets_in_gg(
x1,
x2)
same_sets_out_gg(
x1,
x2) =
same_sets_out_gg
U5_gg(
x1,
x2,
x3,
x4) =
U5_gg(
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
U6_gg(
x1,
x2,
x3,
x4) =
U6_gg(
x4)
perm1_out_gg(
x1,
x2) =
perm1_out_gg
MEMBER_IN_GG(
x1,
x2) =
MEMBER_IN_GG(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MEMBER_IN_GG(X, .(X4, T)) → MEMBER_IN_GG(X, T)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MEMBER_IN_GG(X, .(X4, T)) → MEMBER_IN_GG(X, T)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- MEMBER_IN_GG(X, .(X4, T)) → MEMBER_IN_GG(X, T)
The graph contains the following edges 1 >= 1, 2 > 2
(13) YES
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
U5_GG(X, Xs, L, member_out_gg(X, L)) → SAME_SETS_IN_GG(Xs, L)
SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(X, Xs, L, member_in_gg(X, L))
The TRS R consists of the following rules:
perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X1, Xs), .(X2, Ys)) → U3_gg(X1, Xs, X2, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X1, Xs, X2, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X1, Xs), .(X2, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X5) → same_sets_out_gg([], X5)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, T)) → U4_gg(X, X4, T, member_in_gg(X, T))
U4_gg(X, X4, T, member_out_gg(X, T)) → member_out_gg(X, .(X4, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)
The argument filtering Pi contains the following mapping:
perm1_in_gg(
x1,
x2) =
perm1_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
eq_len1_in_gg(
x1,
x2) =
eq_len1_in_gg(
x1,
x2)
[] =
[]
eq_len1_out_gg(
x1,
x2) =
eq_len1_out_gg
.(
x1,
x2) =
.(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5) =
U3_gg(
x5)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x3)
same_sets_in_gg(
x1,
x2) =
same_sets_in_gg(
x1,
x2)
same_sets_out_gg(
x1,
x2) =
same_sets_out_gg
U5_gg(
x1,
x2,
x3,
x4) =
U5_gg(
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
U6_gg(
x1,
x2,
x3,
x4) =
U6_gg(
x4)
perm1_out_gg(
x1,
x2) =
perm1_out_gg
SAME_SETS_IN_GG(
x1,
x2) =
SAME_SETS_IN_GG(
x1,
x2)
U5_GG(
x1,
x2,
x3,
x4) =
U5_GG(
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(15) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
U5_GG(X, Xs, L, member_out_gg(X, L)) → SAME_SETS_IN_GG(Xs, L)
SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(X, Xs, L, member_in_gg(X, L))
The TRS R consists of the following rules:
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, T)) → U4_gg(X, X4, T, member_in_gg(X, T))
U4_gg(X, X4, T, member_out_gg(X, T)) → member_out_gg(X, .(X4, T))
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
SAME_SETS_IN_GG(
x1,
x2) =
SAME_SETS_IN_GG(
x1,
x2)
U5_GG(
x1,
x2,
x3,
x4) =
U5_GG(
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U5_GG(Xs, L, member_out_gg) → SAME_SETS_IN_GG(Xs, L)
SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(Xs, L, member_in_gg(X, L))
The TRS R consists of the following rules:
member_in_gg(X, .(X, X3)) → member_out_gg
member_in_gg(X, .(X4, T)) → U4_gg(member_in_gg(X, T))
U4_gg(member_out_gg) → member_out_gg
The set Q consists of the following terms:
member_in_gg(x0, x1)
U4_gg(x0)
We have to consider all (P,Q,R)-chains.
(19) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(Xs, L, member_in_gg(X, L))
The graph contains the following edges 1 > 1, 2 >= 2
- U5_GG(Xs, L, member_out_gg) → SAME_SETS_IN_GG(Xs, L)
The graph contains the following edges 1 >= 1, 2 >= 2
(20) YES
(21) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
EQ_LEN1_IN_GG(.(X1, Xs), .(X2, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)
The TRS R consists of the following rules:
perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X1, Xs), .(X2, Ys)) → U3_gg(X1, Xs, X2, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X1, Xs, X2, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X1, Xs), .(X2, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X5) → same_sets_out_gg([], X5)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, T)) → U4_gg(X, X4, T, member_in_gg(X, T))
U4_gg(X, X4, T, member_out_gg(X, T)) → member_out_gg(X, .(X4, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)
The argument filtering Pi contains the following mapping:
perm1_in_gg(
x1,
x2) =
perm1_in_gg(
x1,
x2)
U1_gg(
x1,
x2,
x3) =
U1_gg(
x1,
x2,
x3)
eq_len1_in_gg(
x1,
x2) =
eq_len1_in_gg(
x1,
x2)
[] =
[]
eq_len1_out_gg(
x1,
x2) =
eq_len1_out_gg
.(
x1,
x2) =
.(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5) =
U3_gg(
x5)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x3)
same_sets_in_gg(
x1,
x2) =
same_sets_in_gg(
x1,
x2)
same_sets_out_gg(
x1,
x2) =
same_sets_out_gg
U5_gg(
x1,
x2,
x3,
x4) =
U5_gg(
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
U6_gg(
x1,
x2,
x3,
x4) =
U6_gg(
x4)
perm1_out_gg(
x1,
x2) =
perm1_out_gg
EQ_LEN1_IN_GG(
x1,
x2) =
EQ_LEN1_IN_GG(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(22) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(23) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
EQ_LEN1_IN_GG(.(X1, Xs), .(X2, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(24) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQ_LEN1_IN_GG(.(X1, Xs), .(X2, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(26) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- EQ_LEN1_IN_GG(.(X1, Xs), .(X2, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)
The graph contains the following edges 1 > 1, 2 > 2
(27) YES